Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    f(0)  → s(0)
2:    f(s(0))  → s(0)
3:    f(s(s(x)))  → f(f(s(x)))
There are 2 dependency pairs:
4:    F(s(s(x)))  → F(f(s(x)))
5:    F(s(s(x)))  → F(s(x))
Consider the SCC {4,5}. The constraints could not be solved.
Tyrolean Termination Tool  (0.00 seconds)   ---  May 3, 2006